A, B:Type, f:(AB), L:(A List), L2:(B List), b:B.
(map(f;L) = [b / L2])  {f(hd(L)) = b & map(f;tl(L)) = L2} 

latex

Definitions

s = t, x:AB(x), x:A. B(x), type List, Type, map(f;as), tl(l), #$n, firstn(n;as), nth_tl(n;as), hd(l), f(a), x:A  B(x), P & Q, t  T, A List, {T}, P  Q, , [], [car / cdr], n - m, if a<b then c else d, i <z j, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , rec-case(a) of [] => s | x::y => z.t(x;y;z), x.A(x), Y, i z j, False, Void, , ||as||, n+m, A  B, i  j , {x:A| B(x)} , a < b, A

Lemmas

ge wf, tl wf, hd wf, non neg length, map length, length wf1, guard wf, map wf, map is append